package naruto.core;

import java.io.File;
import java.io.IOException;
import java.io.InputStreamReader;
import java.io.PrintWriter;
import java.util.*;
import naruto.datastructures.criteria.*;
import naruto.datastructures.graph.*;
import naruto.datastructures.instruction.*;
import naruto.datastructures.trace.*;
import naruto.dynamicanalysis.tracing.*;
import naruto.statisanalysis.slicing.*;

/**
 *
 * @author nacuong
 */
public class Main {
  static String executableFile;
  static Vector<String[]> inputs = new Vector<String[]>();
  static Vector<Hashtable<String,String>> methodToNameSet = new Vector<Hashtable<String,String>>();
  static Vector<String> ltlSpecifications = new Vector<String>();
  static Vector<Criteria> criteriaSet = new Vector<Criteria>();

  public static void main(String[] args){
    /* process input */
    System.out.println("Process Input");
    processInput(args);
    /* accumulate criterion */
    System.out.println("Accumulate Criterion");
    accumulateCompleteCriterion();
    /* build if complete model*/
    System.out.println("Build If-complete Models");
    Vector<IfCompleteModel> icModels = buildingModels();
    /* write model to dot file */
    System.out.println("Print Models to Dot Files");
    dotModels(icModels);
    /* write model to smv file */
    System.out.println("Print Models to Smv Files");
    smvModels(icModels);
    /* verify model to get buggy traces */
    System.out.println("Verifying Models");
    Vector<Vector<Integer>> buggyTraces = verifyModels(icModels.size());
    /* generate criteria for slicing */
    System.out.println("Printing Slice Criteria Files");
    Vector<Integer> criteriaIndex = generateSliceCriteria(icModels, buggyTraces);
    /* slice program using indus */
    System.out.println("Slicing Programs");
    slicePrograms(criteriaIndex);
    /* produce program slices from indus results*/
    System.out.println("Produce Slices");
    generateSlices(criteriaIndex);
    /* produce inputs */
    System.out.println("Generating Inputs");
    generateInputs(criteriaIndex);
  }


  /**
   * Get information about jpf_inputs, ltl_specifications, method_to_name_map and criteria_set from
   * the inputs and criteria file.
   */
  public static void processInput(String[] args){
    executableFile = args[0];
    String inputFilePath = args[1];
    String criteriaFilePath = args[2];
    processInputFile(inputFilePath, executableFile, inputs);
    processCriteraFile(criteriaFilePath, methodToNameSet, ltlSpecifications, criteriaSet);
  }

  /**
   * Get a vector of input array from an input file.
   * Input file must contains each input array on seperated lines.
   * @param inputFilePath absolute path of the input file
   * @param inputs vector of input string array
   */
  private static void processInputFile(String inputFilePath, String executableFile, Vector<String[]> inputs){
    try{
      Scanner scanner = new Scanner(new File(inputFilePath));
      while (scanner.hasNext()){
        String[] input = scanner.nextLine().split(" ");
        String[] jpfInput = new String[input.length+1];
        jpfInput[0] = executableFile;
        for (int inx = 0; inx < input.length; inx++)
          jpfInput[inx+1] = input[inx];
        inputs.add(jpfInput);
      }
    } catch (IOException e){
      System.out.println(e);
    }
  }

  /**
   * Get method to name map, ltl specifications and the criteria set from the criteria file.
   * @param criteriaFilePath absolute path of the criteria file
   * @param methodToNameSet the map from method_real_name to mock_method_name
   * @param ltlSpecifications the vector of ltl specification
   * @param criteriaSet the vector of criteria
   */
  private static void processCriteraFile(String criteriaFilePath, Vector<Hashtable<String,String>> methodToNameSet,
          Vector<String> ltlSpecifications, Vector<Criteria> criteriaSet) {
    try {
      Scanner scanner = new Scanner(new File(criteriaFilePath));
      while (scanner.hasNext()){
        Hashtable<String,String> methodToName = new Hashtable<String,String>();
        Criteria criteria = new Criteria();
        boolean readNextSpec = false;
        while (!readNextSpec){
          String map = scanner.nextLine();  /* a map should be in form mock_name=real_method_name */
          String[] pair = map.split(":=");
          String first = pair[0];           /* first should be the mock_name, or spec in case of specfication line */
          String second = pair[1];          /* second should be the real_method_name, or ltl in case of specification line */
          if (first.equals("spec")){
            ltlSpecifications.add(second);
            readNextSpec = true;
          } else {
            methodToName.put(second, first);
            criteria.add(new MethodCallCriterion(second));
          }
        }
        methodToNameSet.add(methodToName);
        criteriaSet.add(criteria);
      }
    } catch (IOException e){
      System.out.println(e);
    }
  }
  
  /**
   * The given criteria does not contain some if instruction that we want to keep track with during execution.
   * The interesting if instructions include those whose complete segment contains a method that appear in
   * the original criteria.
   *
   * We first collect all if_complete_trace of the original method criteria and then extract from it some
   * interesting if instruction that we want to add in the original criteria.
   */
  public static void accumulateCompleteCriterion(){
    IfCompleteTracer icTracer = new IfCompleteTracer(criteriaSet);
    for (String[] input: inputs){
      /* set of if complete traces assosiated with the criteria set */
      Vector<IfCompleteTrace> icTraces = icTracer.run(input);
      for (int inx = 0; inx < icTraces.size(); inx++){
        IfCompleteTrace icTrace = icTraces.get(inx);
        /* the criteria associated with the above if complete trace */
        Criteria criteria = criteriaSet.get(inx);
        for (IfCompleteInstruction icInsn: icTrace){
          /* add each if instruction along the trace as a criterion */
          if (icInsn instanceof IfInstruction && !((IfInstruction)icInsn).isLoopInstruction()){
            InstructionCriterion insnCriterion = new InstructionCriterion(icInsn.getClassName(),
                    icInsn.getMethodInfoName(), icInsn.getOffset());
            if (!criteria.contains(insnCriterion))
              criteria.add(insnCriterion);
          }
        }
      }
    }
  }

  /**
   * Build if complete models from the input set and criteria set. The number of generated
   * if complete model should be equal to the number of criteria.
   * @return vector of if complete model built from the inputSet and criteriaSet.
   */
  public static Vector<IfCompleteModel> buildingModels(){
    IfCompleteTracer icTracer = new IfCompleteTracer(criteriaSet);
    Vector<IfCompleteModel> icModels = new Vector<IfCompleteModel>();
    for (int inx = 0; inx < criteriaSet.size(); inx++)
      icModels.add(new IfCompleteModel());

    for (String[] input: inputs){
      Vector<IfCompleteTrace> icTraces = icTracer.run(input);
      for (int inx = 0; inx < icTraces.size(); inx++){
        IfCompleteTrace icTrace = icTraces.get(inx);
        IfCompleteModel icModel = icModels.get(inx);
        icModel.mergeTrace(icTrace);
      }
    }

    for (IfCompleteModel icModel: icModels)
      icModel.refine();

    return icModels;
  }

  /**
   * Prints all if-complete models in dot form to absolute path folder naruto/models.
   * @param icModels if-comoplete model vector to be printed
   */
  public static void dotModels(Vector<IfCompleteModel> icModels){
    String dotDirPath = "naruto/models/";
    for (int inx = 0; inx < icModels.size(); inx++){
      String dotFilePath = dotDirPath + "model"+inx+".dot";
      IfCompleteModel icModel = icModels.get(inx);
      icModel.toDot(dotFilePath);
    }
  }

/**
 * Prints all if-complete models in smv form to absolute path folder naruto/smvs
 * @param icModels if-comoplete model vector to be printed
 */
  public static void smvModels(Vector<IfCompleteModel> icModels){
    String smvDirPath = "naruto/smvs/";
    for (int inx = 0; inx < icModels.size(); inx++){
      String smvFilePath = smvDirPath + "model"+inx+".smv";
      IfCompleteModel icModel = icModels.get(inx);
      Hashtable<String,String> methodToName = methodToNameSet.get(inx);
      String ltlSpecification = ltlSpecifications.get(inx);
      icModel.toSMV(smvFilePath, ltlSpecification, methodToName);
    }
  }

  /**
   * Verify all if-complete model smv files in naruto/smvs folder. The number of
   * model to be verified is given to identify the index of model smv file.
   * @param modelNo the number of model to be verified. 
   * @return
   */
  public static Vector<Vector<Integer>> verifyModels(int modelNo){
    Vector<Vector<Integer>> buggyTraces = new Vector<Vector<Integer>>();
    Runtime run = Runtime.getRuntime();
    for (int inx = 0; inx < modelNo; inx++){
      String exec = "nusmv naruto/smvs/model" + inx + ".smv";
      Vector<Integer> buggyTrace = new Vector<Integer>();
      buggyTraces.add(buggyTrace);
      try {
        Process process = run.exec(exec);
        Scanner sc = new Scanner(new InputStreamReader(process.getInputStream()));
        boolean verifyResult = true;

        /* check whether nusmv outputs true or false in the line of -- specification */
        while (true && sc.hasNext()){
          String smvOutput = sc.nextLine().trim();
          if (smvOutput != null && smvOutput.contains("-- specification")){
            String[] words = smvOutput.split(" ");
            verifyResult = words[words.length-1].equals("true");
            break;
          }
        }

        /* get buggy traces from nusmv counterexample */
        if (verifyResult == false){
          while (sc.hasNext()){
            String smvOutput = sc.nextLine().trim();
            if (smvOutput.startsWith("state = node"))
              buggyTrace.add(Integer.parseInt(smvOutput.replace("state = node", "")));
          }
        }
      } catch (IOException e){
        System.out.println(e);
      }
    }

    return buggyTraces;
  }

  /**
   * Generate criteria file for buggy traces in naruto/slices.
   * @param icModels
   * @param buggyTraces
   */
  public static Vector<Integer> generateSliceCriteria(Vector<IfCompleteModel> icModels, Vector<Vector<Integer>> buggyTraces) {
    String sliceDirPath = "naruto/slices/";
    Vector<Integer> criteriaIndex = new Vector<Integer>();
    try {
      for (int inx = 0; inx < icModels.size(); inx++) {
        IfCompleteModel icModel = icModels.get(inx);
        Vector<Integer> buggyTrace = buggyTraces.get(inx);
        if (buggyTrace.size() > 0) {
          String sliceCriteriaFilePath = sliceDirPath + "criteria" + inx + ".indus";
          criteriaIndex.add(inx);
          File criteriaFile = new File(sliceCriteriaFilePath);
          criteriaFile.delete();
          criteriaFile.createNewFile();
          PrintWriter pw = new PrintWriter(criteriaFile.getAbsolutePath());
          String javaFileName = null;
          for (int nodeId : buggyTrace) {
            if (nodeId < icModel.size()){
              IfCompleteNode icNode = icModel.get(nodeId);
              if (icNode instanceof IfNode) {
                String className = icNode.getInstruction().getClassName();
                if (!className.equals(javaFileName)){
                  if (javaFileName != null)
                    pw.println();
                  pw.print(className + "=" + icNode.getInstruction().getSourceLineNumber());
                  javaFileName = className;
                } else
                  pw.print("," + icNode.getInstruction().getSourceLineNumber());
              }
            }
          }
          pw.close();
        }
      }
    } catch (IOException e) {
      System.out.println(e);
    }

    return criteriaIndex;
  }

  public static void slicePrograms(Vector<Integer> criteriaSetIndex){
    String sliceDirPath = "naruto/slices/";
    Runtime run = Runtime.getRuntime();
    try {
      for (int criteriaIndex: criteriaSetIndex){
        String sliceOutDir = sliceDirPath + "out" + criteriaIndex;
        (new File(sliceOutDir)).mkdir();
        String criteriaFile = sliceDirPath + "criteria" + criteriaIndex + ".indus";
        String classPath = "classes;lib/indus.zip";
        String java4Home = "d:/soft.bin/java/j2sdk1.4.2_19";
        String sootClassPath = "classes;d:/soft.bin/java/test;" +
                java4Home + "/jre/lib/resources.jar;" + java4Home + "/jre/lib/jce.jar";
        String configurationFile = sliceDirPath + "default_slicer_configuration.xml";
        String scopeFile = sliceDirPath + "scope.xml";
        String exec = "java -Xmx1000M -cp " + classPath + " edu.ksu.cis.indus.tools.slicer.SliceXMLizerCLI" +
                " -p " + sootClassPath + " -S " + scopeFile + " -r -J -c " + configurationFile + " -o " + sliceOutDir + " -l " + criteriaFile + " " + executableFile;
        Process process = run.exec(exec);
        //System.out.println(exec);

//         debug
        Scanner sc = new Scanner(new InputStreamReader(process.getErrorStream()));
        while (sc.hasNext())
          sc.nextLine();
      }
    } catch (IOException e){
      System.out.println(e);
    } 
  }

  public static void generateSlices(Vector<Integer> criteriaSetIndex){
    String sliceDirPath = "naruto/slices/";
    String sourceDir = "src";
    Runtime run = Runtime.getRuntime();
    try {
      String buildFilePath = sliceDirPath + "build.xml";
      for (int criteriaIndex: criteriaSetIndex){
        String sliceOutDir = sliceDirPath + "out" + criteriaIndex;
        String sliceDir = sliceDirPath + "slice" + criteriaIndex;
        (new File(sliceDir)).mkdir();
        SliceResultAnalysis.produceSlices(executableFile, sourceDir, sliceOutDir, sliceDir);
        String moveBuildFile = "cp " + buildFilePath + " " + sliceDir;
        Process process1 = run.exec(moveBuildFile);
				
				//         debug
        Scanner sc1 = new Scanner(new InputStreamReader(process1.getErrorStream()));
        while (sc1.hasNext())
          sc1.nextLine();
					
        String sliceBuildFilePath = sliceDir + "/build.xml";
        String buildAnt = "ant.bat -buildfile " + sliceBuildFilePath;
        Process process2 = run.exec(buildAnt);
        process2.getErrorStream(); // this line ensures that the process has finished running
				
				//         debug
        Scanner sc2 = new Scanner(new InputStreamReader(process2.getErrorStream()));
        while (sc2.hasNext())
          sc2.nextLine();
      }
    } catch (IOException e){
      System.out.println(e);
    } 
  }

  public static void generateInputs(Vector<Integer> criteriaSetIndex){
    String sliceDirPath = "naruto/slices/";
    Runtime run = Runtime.getRuntime();
    String[] oneInput = inputs.get(0);
    int inputLength = oneInput.length;
    String symParamater = "";
    String input = "";
    for (int inx = 1; inx < inputLength; inx++){
      input += " " + oneInput[inx];
      symParamater += "sym";
      if (inx != inputLength-1)
        symParamater += "#";
    }
    try {
      for (int criteriaIndex: criteriaSetIndex){
        String classPath = "lib/javapathfinder.zip;" +
                    "lib/jpfsymc.zip;" +
           "naruto/slices/slice" + criteriaIndex;
        String exec = "java -Xmx1000M -cp " + classPath + " gov.nasa.jpf.JPF "
                + "+vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory "
                + "+vm.classpath=. "
                + "+vm.storage.class= "
                + "+symbolic.method=temp(" + symParamater + ") "
                + "+search.multiple_errors=true "
                + "+jpf.report.console.finished= "
                + executableFile + input;
        Process process = run.exec(exec);
        Scanner sc = new Scanner(new InputStreamReader(process.getInputStream()));
        while (sc.hasNext()) 
          System.out.println(sc.nextLine());
      }

    } catch (IOException e){
      System.out.println(e);
    } 
  }
}
